FDL - Nuprl Lemma : fpf-rename-dom

Nuprl Lemma : fpf-rename-dom

A, C:Type, B:(A

Type), eqa:EqDecider(A), eqc:EqDecider(C), r:(A

C), f:a:A fp

B(a), c:C.
(

c

dom(rename(r;f)))

(

a:A. ((

a

dom(f)) c

(c = r(a))))

Definitions x:A. B(x), x(s), P Q, x dom(f), rename(r;f), x:A. B(x), A c B, t.1, P Q, , P Q, t T, x. t(x), P & Q, a:A fp B(a)

Lemmas iff functionality wrt iff, assert wf, deq-member wf, map wf, l member wf, assert-deq-member, exists functionality wrt iff, cand functionality wrt iff, member map, fpf wf, deq wf